Modern software systems, and in particular web and mobile applications, are the target of increasingly many attacks and attack types. Examples of the attack types may include e.g. cross-site scripting (XSS), cross-application scripting (XAS), SQL injection (SQLi), log forging, etc. Many modern software applications are of increasing size and complexity, and may often include multiple abstraction layers, and large third-party libraries, and may perform nontrivial pointer-based computations. As such, manually testing and examining such software applications for potential security vulnerabilities can be so time consuming as to be impractical. For this reason, there has been an increasing need for, and interest in, automated methods for detection of potential security vulnerabilities. Indeed, static security verification, which may be based on program analysis techniques, and in particular the theory of abstract interpretation, has enjoyed a great deal of success throughout the last decade by being able to scale to large programs and uncover latent vulnerabilities.
However, as software is becoming both larger and more complex, there is a parallel trend of decreases in the usability of security verification tools. One cause for the decrease in the usability of security verification tool may stem from the increased complexity, which may lead to false warnings (aka false positives). Additionally, the size of the software applications, can result in an overwhelming number of reported security vulnerabilities. Combined, these two factors can often lead to enormous security reports, which may include many thousands of warnings, with many, if not most, of the warnings included within the security report being false positives—items that do not actually represent a security vulnerability. The large number or reported security vulnerabilities, many of which may be erroneous, can often be beyond what user, or even a team of users, can effectively manage to review and translate into security enhancing code changes.